a:, b:{...-1}. (a  b) = (-(a  (-b))) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), False, P  Q, A, a  b  T , , , True, T, i > j, P & Q, A  B, {...i}, , P  Q
Lemmas	nat wf, int lower wf, rem bounds 4, nequal wf, rem bounds 1, div rem sum, add mono wrt eq, le wf, true wf, squash wf, add mono wrt lt, add mono wrt le, lt transitivity 2, mul cancel in lt, minus functionality wrt lt